package com.googlecode.kipler.satisfiability.completion.rule.individual;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.BasicWcsInterpolationData;
import com.googlecode.kipler.container.dl.LabelManager;
import com.googlecode.kipler.satisfiability.blocking.abox.ABoxBlockingStrategy;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.concept.ConceptName;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.ConceptDefinition;

/**
 * 
 * @author İnanç Seylan
 * 
 */
public class PositiveConceptDefinitionRule extends ABoxRule {
	private ABox aBox;

	private boolean applied;

	private ABoxBlockingStrategy blocking;

	public boolean isApplied() {
		return applied;
	}

	public PositiveConceptDefinitionRule(ABoxBlockingStrategy blocking) {
		setBlocking(blocking);
	}

	public ABoxBlockingStrategy getBlocking() {
		return blocking;
	}

	public void setBlocking(ABoxBlockingStrategy blocking) {
		this.blocking = blocking;
	}

	@Override
	public void apply() throws UnsatisfiableException {
		applied = false;
		aBox = getWorld().getABox();
		if (!getBlocking().isIndirectlyBlocked(aBox, getIndividual().getName())) {
			for (ConceptDefinition conDef : getWorld().getTBox().getGeneral()
					.getPositiveGCEs()) {
				if (conDef.getRhs().equals(ConceptName.topConcept())) {
					applyEquality(conDef);
				}
			}
		}
	}

	private void applyEquality(ConceptDefinition conDef)
			throws UnsatisfiableException {
		Concept concept = conDef.getLhs();
		ConceptAssertion ca = new ConceptAssertion(concept, getIndividual()
				.getName());
		if (!aBox.contains(ca)) {
			if (getWcs().getReasoner().getProfile().isInterpolationEnabled()) {
				LabelManager labelMan = ((BasicWcsInterpolationData) getWcs()
						.getData()).getLabelManager();
				labelMan.copyLabel(conDef, ca);
			}
			aBox.add(ca);
			applied = true;
			getWcs()
					.getData()
					.getLogger()
					.info(
							"WCS "
									+ getWcs().getId()
									+ " Positive concept definition rule: Adding "
									+ ca);
		}
	}
}
